Fix System S rejecting kernel signatures: evaluate hoisted declare typeforms - #63

Fixes #62

Root cause

boot.lua's hoist_tail pulls the trailing (declare Name Typeform) block of types.kl out of the kernel chunk so the type-theory cost of the 161 kernel signatures can be cached. But Typeform is a KL expression — an rcons constructor tree such as (cons number (cons --> (cons number ()))) — which the inline form would evaluate before declare sees it. The hoist passed the unevaluated AST straight to declare, so every hoisted signature closure registered in shen.*sigf* unified goal types against the literal (cons ...) s-expression instead of the type (number --> (number --> number)), and never matched anything.

The native typecheck engine masked the bug on the shen.typecheck path — it harvests signatures from types.kl independently (typecheck_native.lua) — which is why tc mode looked fine. Anything consulting the real *sigf* closures was broken:

• prolog?-driven shen.system-S queries (the issue's repro): every shen.lookupsig-based judgment failed, visibly + - * / > < >= <= (cons worked only because it has a dedicated System S rule);
• the legacy typecheck path (SHEN_TYPECHECK_NATIVE=off, SHEN_PROLOG_ENGINE=legacy): (shen.typecheck [* 2 3] A) returned false.

Fix

• hoist_tail now evaluates each declare's typeform with a small pure evaluator (cons trees, (intern "..."), self-evaluating atoms) before handing it to declare, matching inline KL semantics exactly. A typeform it cannot prove literal refuses the hoist, so such a form would run inline with full KL semantics instead of being mis-cached.
• CACHE_FORMAT bumped SHENKC3 -> SHENKC4: the kernel cache key does not cover boot.lua, and pre-fix caches contain declare dumps compiled from the unevaluated typeforms; the bump invalidates them.

Verification

• Issue repro now prints true/true/true/true (was false/false/false/true), matching shen-go and shen-cl; verdicts for partial application and negative judgments also cross-checked against shen-go.
• New regression spec test/system_s_sigf_spec.lua (runs under make test): the four issue judgments, partial application, negative cases, and a direct ground-unify of the + closure stored in *sigf*.
• make test: 899 pass, 0 fail across 20 specs.
• make certify (canonical ShenOSKernel suite): 100% pass.
• Verified cold (kernel cache and ~/.cache/shen-lua-fasl cleared, SHEN_FASL=off) and warm (kernel cache + fasl hit) — identical results.
• Downstream: shenlogic tests/oracle-arith.shen under the fixed bin/shen prints SHENLOGIC|ORACLE ARITH PASS.

🤖 Generated with Claude Code